$\forall$$A$, $B$:Type, ${\it eq}_{1}$:EqDecider($A$), ${\it eq}_{2}$:EqDecider($B$), $L$:((:$A$ $\times$ $B$) List). fpf($L$) $\in$ $a$:$A$ fp$\rightarrow$ $B$ List